<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Lists: Working with Structured Data</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Lists<span class="subtitle">Working with Structured Data</span></h1>


<div class="code">

<span class="id" title="keyword">From</span> <span class="id" title="var">LF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Induction.html#"><span class="id" title="library">Induction</span></a>.<br/>
<span class="id" title="keyword">Module</span> <a id="NatList" class="idref" href="#NatList"><span class="id" title="module">NatList</span></a>.<br/>
</div>

<div class="doc">
<a id="lab67"></a><h1 class="section">Pairs of Numbers</h1>

<div class="paragraph"> </div>

 In an <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span> type definition, each constructor can take
    any number of arguments -- none (as with <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">O</span></span>), one (as
    with <span class="inlinecode"><span class="id" title="var">S</span></span>), or more than one (as with <span class="inlinecode"><span class="id" title="var">nybble</span></span>, and here): 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="NatList.natprod" class="idref" href="#NatList.natprod"><span class="id" title="inductive">natprod</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="NatList.pair" class="idref" href="#NatList.pair"><span class="id" title="constructor">pair</span></a> (<a id="n<sub>1</sub>:3" class="idref" href="#n<sub>1</sub>:3"><span class="id" title="binder">n<sub>1</sub></span></a> <a id="n<sub>2</sub>:4" class="idref" href="#n<sub>2</sub>:4"><span class="id" title="binder">n<sub>2</sub></span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/>
</div>

<div class="doc">
This declaration can be read: "The one and only way to
    construct a pair of numbers is by applying the constructor <span class="inlinecode"><span class="id" title="var">pair</span></span>
    to two arguments of type <span class="inlinecode"><span class="id" title="var">nat</span></span>." 
</div>
<div class="code">

<span class="id" title="keyword">Check</span> (<a class="idref" href="Lists.html#NatList.pair"><span class="id" title="constructor">pair</span></a> 3 5) : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>.<br/>
</div>

<div class="doc">
Here are simple functions for extracting the first and
    second components of a pair. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.fst" class="idref" href="#NatList.fst"><span class="id" title="definition">fst</span></a> (<a id="p:5" class="idref" href="#p:5"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#p:5"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <span class="id" title="var">x</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.snd" class="idref" href="#NatList.snd"><span class="id" title="definition">snd</span></a> (<a id="p:7" class="idref" href="#p:7"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#p:7"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> ⇒ <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Compute</span> (<a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> (<a class="idref" href="Lists.html#NatList.pair"><span class="id" title="constructor">pair</span></a> 3 5)).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;3&nbsp;*)</span><br/>
</div>

<div class="doc">
Since pairs will be used heavily in what follows, it is nice
    to be able to write them with the standard mathematical notation
    <span class="inlinecode">(<span class="id" title="var">x</span>,<span class="id" title="var">y</span>)</span> instead of <span class="inlinecode"><span class="id" title="var">pair</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>.  We can tell Coq to allow this with
    a <span class="inlinecode"><span class="id" title="keyword">Notation</span></span> declaration. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="3797a507925d1a8b76f7e11d37069da<sub>7</sub>" class="idref" href="#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">&quot;</span></a>( x , y )" := (<a class="idref" href="Lists.html#NatList.pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>).<br/>
</div>

<div class="doc">
The new notation can be used both in expressions and in pattern
    matches. 
</div>
<div class="code">

<span class="id" title="keyword">Compute</span> (<a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a>3<a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a>5<a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.fst'" class="idref" href="#NatList.fst'"><span class="id" title="definition">fst'</span></a> (<a id="p:9" class="idref" href="#p:9"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#p:9"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><span class="id" title="var">y</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a> ⇒ <span class="id" title="var">x</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.snd'" class="idref" href="#NatList.snd'"><span class="id" title="definition">snd'</span></a> (<a id="p:11" class="idref" href="#p:11"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#p:11"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><span class="id" title="var">y</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a> ⇒ <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.swap_pair" class="idref" href="#NatList.swap_pair"><span class="id" title="definition">swap_pair</span></a> (<a id="p:13" class="idref" href="#p:13"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>) : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#p:13"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><span class="id" title="var">y</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><span class="id" title="var">x</span><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Note that pattern-matching on a pair (with parentheses: <span class="inlinecode">(<span class="id" title="var">x</span>,</span> <span class="inlinecode"><span class="id" title="var">y</span>)</span>)
    is not to be confused with the "multiple pattern" syntax (with no
    parentheses: <span class="inlinecode"><span class="id" title="var">x</span>,</span> <span class="inlinecode"><span class="id" title="var">y</span></span>) that we have seen previously.  The above
    examples illustrate pattern matching on a pair with elements <span class="inlinecode"><span class="id" title="var">x</span></span>
    and <span class="inlinecode"><span class="id" title="var">y</span></span>, whereas, for example, the definition of <span class="inlinecode"><span class="id" title="var">minus</span></span> in
    <a href="Basics.html"><span class="inlineref">Basics</span></a> performs pattern matching on the values <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">m</span></span>:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Fixpoint</span> <span class="id" title="var">minus</span> (<span class="id" title="var">n</span> <span class="id" title="var">m</span> : <span class="id" title="var">nat</span>) : <span class="id" title="var">nat</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">n</span>, <span class="id" title="var">m</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">O</span>   , <span class="id" title="var">_</span>    ⇒ <span class="id" title="var">O</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">S</span> <span class="id" title="var">_</span> , <span class="id" title="var">O</span>    ⇒ <span class="id" title="var">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">S</span> <span class="id" title="var">n'</span>, <span class="id" title="var">S</span> <span class="id" title="var">m'</span> ⇒ <span class="id" title="var">minus</span> <span class="id" title="var">n'</span> <span class="id" title="var">m'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.
</span>    The distinction is minor, but it is worth knowing that they
    are not the same. For instance, the following definitions are
    ill-formed:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Can't&nbsp;match&nbsp;on&nbsp;a&nbsp;pair&nbsp;with&nbsp;multiple&nbsp;patterns:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <span class="id" title="var">bad_fst</span> (<span class="id" title="var">p</span> : <span class="id" title="var">natprod</span>) : <span class="id" title="var">nat</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">p</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">x</span>, <span class="id" title="var">y</span> ⇒ <span class="id" title="var">x</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Can't&nbsp;match&nbsp;on&nbsp;multiple&nbsp;values&nbsp;with&nbsp;pair&nbsp;patterns:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <span class="id" title="var">bad_minus</span> (<span class="id" title="var">n</span> <span class="id" title="var">m</span> : <span class="id" title="var">nat</span>) : <span class="id" title="var">nat</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">n</span>, <span class="id" title="var">m</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" title="var">O</span>   , <span class="id" title="var">_</span>   ) ⇒ <span class="id" title="var">O</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" title="var">S</span> <span class="id" title="var">_</span> , <span class="id" title="var">O</span>   ) ⇒ <span class="id" title="var">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" title="var">S</span> <span class="id" title="var">n'</span>, <span class="id" title="var">S</span> <span class="id" title="var">m'</span>) ⇒ <span class="id" title="var">bad_minus</span> <span class="id" title="var">n'</span> <span class="id" title="var">m'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.
</span>
<div class="paragraph"> </div>

 Now let's try to prove a few simple facts about pairs.

<div class="paragraph"> </div>

    If we state properties of pairs in a slightly peculiar way, we can
    sometimes complete their proofs with just reflexivity (and its
    built-in simplification): 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.surjective_pairing'" class="idref" href="#NatList.surjective_pairing'"><span class="id" title="lemma">surjective_pairing'</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:15" class="idref" href="#n:15"><span class="id" title="binder">n</span></a> <a id="m:16" class="idref" href="#m:16"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#n:15"><span class="id" title="variable">n</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Lists.html#m:16"><span class="id" title="variable">m</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#n:15"><span class="id" title="variable">n</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Lists.html#m:16"><span class="id" title="variable">m</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">),</span></a> <a class="idref" href="Lists.html#NatList.snd"><span class="id" title="definition">snd</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#n:15"><span class="id" title="variable">n</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Lists.html#m:16"><span class="id" title="variable">m</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">))</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
But <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span> is not enough if we state the lemma in a more
    natural way: 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.surjective_pairing_stuck" class="idref" href="#NatList.surjective_pairing_stuck"><span class="id" title="lemma">surjective_pairing_stuck</span></a> : <span class="id" title="keyword">∀</span> (<a id="p:17" class="idref" href="#p:17"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#p:17"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> <a class="idref" href="Lists.html#p:17"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Lists.html#NatList.snd"><span class="id" title="definition">snd</span></a> <a class="idref" href="Lists.html#p:17"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="comment">(*&nbsp;Doesn't&nbsp;reduce&nbsp;anything!&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Instead, we need to expose the structure of <span class="inlinecode"><span class="id" title="var">p</span></span> so that
    <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> can perform the pattern match in <span class="inlinecode"><span class="id" title="var">fst</span></span> and <span class="inlinecode"><span class="id" title="var">snd</span></span>.  We can
    do this with <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.surjective_pairing" class="idref" href="#NatList.surjective_pairing"><span class="id" title="lemma">surjective_pairing</span></a> : <span class="id" title="keyword">∀</span> (<a id="p:18" class="idref" href="#p:18"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#p:18"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> <a class="idref" href="Lists.html#p:18"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Lists.html#NatList.snd"><span class="id" title="definition">snd</span></a> <a class="idref" href="Lists.html#p:18"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">p</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">p</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">n</span> <span class="id" title="var">m</span>]. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Notice that, unlike its behavior with <span class="inlinecode"><span class="id" title="var">nat</span></span>s, where it
    generates two subgoals, <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> generates just one subgoal
    here.  That's because <span class="inlinecode"><span class="id" title="var">natprod</span></span>s can only be constructed in one
    way. 
<div class="paragraph"> </div>

<a id="lab68"></a><h4 class="section">Exercise: 1 star, standard (snd_fst_is_swap)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="NatList.snd_fst_is_swap" class="idref" href="#NatList.snd_fst_is_swap"><span class="id" title="lemma">snd_fst_is_swap</span></a> : <span class="id" title="keyword">∀</span> (<a id="p:19" class="idref" href="#p:19"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.snd"><span class="id" title="definition">snd</span></a> <a class="idref" href="Lists.html#p:19"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> <a class="idref" href="Lists.html#p:19"><span class="id" title="variable">p</span></a><a class="idref" href="Lists.html#3797a507925d1a8b76f7e11d37069da<sub>7</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.swap_pair"><span class="id" title="definition">swap_pair</span></a> <a class="idref" href="Lists.html#p:19"><span class="id" title="variable">p</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab69"></a><h4 class="section">Exercise: 1 star, standard, optional (fst_swap_is_snd)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="NatList.fst_swap_is_snd" class="idref" href="#NatList.fst_swap_is_snd"><span class="id" title="lemma">fst_swap_is_snd</span></a> : <span class="id" title="keyword">∀</span> (<a id="p:20" class="idref" href="#p:20"><span class="id" title="binder">p</span></a> : <a class="idref" href="Lists.html#NatList.natprod"><span class="id" title="inductive">natprod</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.fst"><span class="id" title="definition">fst</span></a> (<a class="idref" href="Lists.html#NatList.swap_pair"><span class="id" title="definition">swap_pair</span></a> <a class="idref" href="Lists.html#p:20"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.snd"><span class="id" title="definition">snd</span></a> <a class="idref" href="Lists.html#p:20"><span class="id" title="variable">p</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab70"></a><h1 class="section">Lists of Numbers</h1>

<div class="paragraph"> </div>

 Generalizing the definition of pairs, we can describe the
    type of <i>lists</i> of numbers like this: "A list is either the empty
    list or else a pair of a number and another list." 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="NatList.natlist" class="idref" href="#NatList.natlist"><span class="id" title="inductive">natlist</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="NatList.nil" class="idref" href="#NatList.nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <a id="NatList.cons" class="idref" href="#NatList.cons"><span class="id" title="constructor">cons</span></a> (<a id="n:23" class="idref" href="#n:23"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="l:24" class="idref" href="#l:24"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#natlist:21"><span class="id" title="inductive">natlist</span></a>).<br/>
</div>

<div class="doc">
For example, here is a three-element list: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.mylist" class="idref" href="#NatList.mylist"><span class="id" title="definition">mylist</span></a> := <a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> 1 (<a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> 2 (<a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> 3 <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>)).<br/>
</div>

<div class="doc">
As with pairs, it is more convenient to write lists in
    familiar programming notation.  The following declarations
    allow us to use <span class="inlinecode">::</span> as an infix <span class="inlinecode"><span class="id" title="var">cons</span></span> operator and square
    brackets as an "outfix" notation for constructing lists. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="NatList.:::x_'::'_x" class="idref" href="#NatList.:::x_'::'_x"><span class="id" title="notation">&quot;</span></a>x :: l" := (<a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">x</span> <span class="id" title="var">l</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>" class="idref" href="#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">&quot;</span></a>[ ]" := <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="62815778618d6f51cd0f9ac90bf0e8be" class="idref" href="#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">&quot;</span></a>[ x ; .. ; y ]" := (<a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">x</span> .. (<a class="idref" href="Lists.html#NatList.cons"><span class="id" title="constructor">cons</span></a> <span class="id" title="var">y</span> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>) ..).<br/>
</div>

<div class="doc">
It is not necessary to understand the details of these
    declarations, but here is roughly what's going on in case you are
    interested.  The "<span class="inlinecode"><span class="id" title="tactic">right</span></span> <span class="inlinecode"><span class="id" title="keyword">associativity</span></span>" annotation tells Coq how to
    parenthesize expressions involving multiple uses of <span class="inlinecode">::</span> so that,
    for example, the next three declarations mean exactly the same
    thing: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.mylist1" class="idref" href="#NatList.mylist1"><span class="id" title="definition">mylist1</span></a> := 1 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">(</span></a>2 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">(</span></a>3 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a><a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">))</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="NatList.mylist2" class="idref" href="#NatList.mylist2"><span class="id" title="definition">mylist2</span></a> := 1 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> 2 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> 3 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a id="NatList.mylist3" class="idref" href="#NatList.mylist3"><span class="id" title="definition">mylist3</span></a> := <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
</div>

<div class="doc">
The "<span class="inlinecode"><span class="id" title="tactic">at</span></span> <span class="inlinecode"><span class="id" title="keyword">level</span></span> <span class="inlinecode">60</span>" part tells Coq how to parenthesize
    expressions that involve both <span class="inlinecode">::</span> and some other infix operator.
    For example, since we defined <span class="inlinecode">+</span> as infix notation for the <span class="inlinecode"><span class="id" title="var">plus</span></span>
    function at level 50,
<br/>
<span class="inlinecode">&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> "x + y" := (<span class="id" title="var">plus</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).
</span>    the <span class="inlinecode">+</span> operator will bind tighter than <span class="inlinecode">::</span>, so <span class="inlinecode">1</span> <span class="inlinecode">+</span> <span class="inlinecode">2</span> <span class="inlinecode">::</span> <span class="inlinecode">[3]</span>
    will be parsed, as we'd expect, as <span class="inlinecode">(1</span> <span class="inlinecode">+</span> <span class="inlinecode">2)</span> <span class="inlinecode">::</span> <span class="inlinecode">[3]</span> rather than
    <span class="inlinecode">1</span> <span class="inlinecode">+</span> <span class="inlinecode">(2</span> <span class="inlinecode">::</span> <span class="inlinecode">[3])</span>.

<div class="paragraph"> </div>

    (Expressions like "<span class="inlinecode">1</span> <span class="inlinecode">+</span> <span class="inlinecode">2</span> <span class="inlinecode">::</span> <span class="inlinecode">[3]</span>" can be a little confusing when
    you read them in a <span class="inlinecode">.<span class="id" title="var">v</span></span> file.  The inner brackets, around 3, indicate
    a list, but the outer brackets, which are invisible in the HTML
    rendering, are there to instruct the "coqdoc" tool that the bracketed
    part should be displayed as Coq code rather than running text.)

<div class="paragraph"> </div>

    The second and third <span class="inlinecode"><span class="id" title="keyword">Notation</span></span> declarations above introduce the
    standard square-bracket notation for lists; the right-hand side of
    the third one illustrates Coq's syntax for declaring n-ary
    notations and translating them to nested sequences of binary
    constructors. 
<div class="paragraph"> </div>

<a id="lab71"></a><h3 class="section">Repeat</h3>

<div class="paragraph"> </div>

 Next let's look at several functions for constructing and
    manipulating lists.  First, the <span class="inlinecode"><span class="id" title="tactic">repeat</span></span> function takes a number
    <span class="inlinecode"><span class="id" title="var">n</span></span> and a <span class="inlinecode"><span class="id" title="var">count</span></span> and returns a list of length <span class="inlinecode"><span class="id" title="var">count</span></span> in which
    every element is <span class="inlinecode"><span class="id" title="var">n</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.repeat" class="idref" href="#NatList.repeat"><span class="id" title="definition">repeat</span></a> (<a id="n:25" class="idref" href="#n:25"><span class="id" title="binder">n</span></a> <a id="count:26" class="idref" href="#count:26"><span class="id" title="binder">count</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#count:26"><span class="id" title="variable">count</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">count'</span> ⇒ <a class="idref" href="Lists.html#n:25"><span class="id" title="variable">n</span></a> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#repeat:27"><span class="id" title="definition">repeat</span></a> <a class="idref" href="Lists.html#n:25"><span class="id" title="variable">n</span></a> <span class="id" title="var">count'</span><a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab72"></a><h3 class="section">Length</h3>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="var">length</span></span> function calculates the length of a list. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.length" class="idref" href="#NatList.length"><span class="id" title="definition">length</span></a> (<a id="l:29" class="idref" href="#l:29"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:29"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Lists.html#length:30"><span class="id" title="definition">length</span></a> <span class="id" title="var">t</span>)<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab73"></a><h3 class="section">Append</h3>

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="var">app</span></span> function concatenates (appends) two lists. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.app" class="idref" href="#NatList.app"><span class="id" title="definition">app</span></a> (<a id="l<sub>1</sub>:32" class="idref" href="#l<sub>1</sub>:32"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:33" class="idref" href="#l<sub>2</sub>:33"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l<sub>1</sub>:32"><span class="id" title="variable">l<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>    ⇒ <a class="idref" href="Lists.html#l<sub>2</sub>:33"><span class="id" title="variable">l<sub>2</sub></span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#app:34"><span class="id" title="definition">app</span></a> <span class="id" title="var">t</span> <a class="idref" href="Lists.html#l<sub>2</sub>:33"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Since <span class="inlinecode"><span class="id" title="var">app</span></span> will be used extensively, it is again convenient
    to have an infix operator for it. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>" class="idref" href="#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">&quot;</span></a>x ++ y" := (<a class="idref" href="Lists.html#NatList.app"><span class="id" title="definition">app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_app1" class="idref" href="#NatList.test_app1"><span class="id" title="definition">test_app1</span></a>:             <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_app2" class="idref" href="#NatList.test_app2"><span class="id" title="definition">test_app2</span></a>:             <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_app3" class="idref" href="#NatList.test_app3"><span class="id" title="definition">test_app3</span></a>:             <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab74"></a><h3 class="section">Head and Tail</h3>

<div class="paragraph"> </div>

 Here are two smaller examples of programming with lists.
    The <span class="inlinecode"><span class="id" title="var">hd</span></span> function returns the first element (the "head") of the
    list, while <span class="inlinecode"><span class="id" title="var">tl</span></span> returns everything but the first element (the
    "tail").  Since the empty list has no first element, we pass
    a default value to be returned in that case.  
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.hd" class="idref" href="#NatList.hd"><span class="id" title="definition">hd</span></a> (<a id="default:36" class="idref" href="#default:36"><span class="id" title="binder">default</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="l:37" class="idref" href="#l:37"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:37"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="Lists.html#default:36"><span class="id" title="variable">default</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <span class="id" title="var">h</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.tl" class="idref" href="#NatList.tl"><span class="id" title="definition">tl</span></a> (<a id="l:39" class="idref" href="#l:39"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:39"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <span class="id" title="var">t</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_hd<sub>1</sub>" class="idref" href="#NatList.test_hd<sub>1</sub>"><span class="id" title="definition">test_hd<sub>1</sub></span></a>:             <a class="idref" href="Lists.html#NatList.hd"><span class="id" title="definition">hd</span></a> 0 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_hd<sub>2</sub>" class="idref" href="#NatList.test_hd<sub>2</sub>"><span class="id" title="definition">test_hd<sub>2</sub></span></a>:             <a class="idref" href="Lists.html#NatList.hd"><span class="id" title="definition">hd</span></a> 0 <a class="idref" href="Lists.html#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_tl" class="idref" href="#NatList.test_tl"><span class="id" title="definition">test_tl</span></a>:              <a class="idref" href="Lists.html#NatList.tl"><span class="id" title="definition">tl</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab75"></a><h3 class="section">Exercises</h3>

<div class="paragraph"> </div>

<a id="lab76"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (list_funs)</h4>
 Complete the definitions of <span class="inlinecode"><span class="id" title="var">nonzeros</span></span>, <span class="inlinecode"><span class="id" title="var">oddmembers</span></span>, and
    <span class="inlinecode"><span class="id" title="var">countoddmembers</span></span> below. Have a look at the tests to understand
    what these functions should do. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.nonzeros" class="idref" href="#NatList.nonzeros"><span class="id" title="definition">nonzeros</span></a> (<a id="l:41" class="idref" href="#l:41"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_nonzeros" class="idref" href="#NatList.test_nonzeros"><span class="id" title="definition">test_nonzeros</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.nonzeros"><span class="id" title="axiom">nonzeros</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="NatList.oddmembers" class="idref" href="#NatList.oddmembers"><span class="id" title="definition">oddmembers</span></a> (<a id="l:43" class="idref" href="#l:43"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_oddmembers" class="idref" href="#NatList.test_oddmembers"><span class="id" title="definition">test_oddmembers</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.oddmembers"><span class="id" title="axiom">oddmembers</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.countoddmembers" class="idref" href="#NatList.countoddmembers"><span class="id" title="definition">countoddmembers</span></a> (<a id="l:45" class="idref" href="#l:45"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_countoddmembers1" class="idref" href="#NatList.test_countoddmembers1"><span class="id" title="definition">test_countoddmembers1</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.countoddmembers"><span class="id" title="axiom">countoddmembers</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 4.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_countoddmembers2" class="idref" href="#NatList.test_countoddmembers2"><span class="id" title="definition">test_countoddmembers2</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.countoddmembers"><span class="id" title="axiom">countoddmembers</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>0<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_countoddmembers3" class="idref" href="#NatList.test_countoddmembers3"><span class="id" title="definition">test_countoddmembers3</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.countoddmembers"><span class="id" title="axiom">countoddmembers</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab77"></a><h4 class="section">Exercise: 3 stars, advanced (alternate)</h4>
 Complete the following definition of <span class="inlinecode"><span class="id" title="var">alternate</span></span>, which
    interleaves two lists into one, alternating between elements taken
    from the first list and elements from the second.  See the tests
    below for more specific examples.

<div class="paragraph"> </div>

    (Note: one natural and elegant way of writing <span class="inlinecode"><span class="id" title="var">alternate</span></span> will
    fail to satisfy Coq's requirement that all <span class="inlinecode"><span class="id" title="keyword">Fixpoint</span></span> definitions
    be "obviously terminating."  If you find yourself in this rut,
    look for a slightly more verbose solution that considers elements
    of both lists at the same time.  One possible solution involves
    defining a new kind of pairs, but this is not the only way.)  
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.alternate" class="idref" href="#NatList.alternate"><span class="id" title="definition">alternate</span></a> (<a id="l<sub>1</sub>:46" class="idref" href="#l<sub>1</sub>:46"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:47" class="idref" href="#l<sub>2</sub>:47"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_alternate1" class="idref" href="#NatList.test_alternate1"><span class="id" title="definition">test_alternate1</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.alternate"><span class="id" title="axiom">alternate</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_alternate2" class="idref" href="#NatList.test_alternate2"><span class="id" title="definition">test_alternate2</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.alternate"><span class="id" title="axiom">alternate</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_alternate3" class="idref" href="#NatList.test_alternate3"><span class="id" title="definition">test_alternate3</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.alternate"><span class="id" title="axiom">alternate</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_alternate4" class="idref" href="#NatList.test_alternate4"><span class="id" title="definition">test_alternate4</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.alternate"><span class="id" title="axiom">alternate</span></a> <a class="idref" href="Lists.html#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">[]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>20<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>30<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>20<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>30<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab78"></a><h3 class="section">Bags via Lists</h3>

<div class="paragraph"> </div>

 A <span class="inlinecode"><span class="id" title="var">bag</span></span> (or <span class="inlinecode"><span class="id" title="var">multiset</span></span>) is like a set, except that each element
    can appear multiple times rather than just once.  One possible
    representation for a bag of numbers is as a list. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.bag" class="idref" href="#NatList.bag"><span class="id" title="definition">bag</span></a> := <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>.<br/>
</div>

<div class="doc">
<a id="lab79"></a><h4 class="section">Exercise: 3 stars, standard, especially useful (bag_functions)</h4>
 Complete the following definitions for the functions
    <span class="inlinecode"><span class="id" title="var">count</span></span>, <span class="inlinecode"><span class="id" title="var">sum</span></span>, <span class="inlinecode"><span class="id" title="var">add</span></span>, and <span class="inlinecode"><span class="id" title="var">member</span></span> for bags. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.count" class="idref" href="#NatList.count"><span class="id" title="definition">count</span></a> (<a id="v:49" class="idref" href="#v:49"><span class="id" title="binder">v</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="s:50" class="idref" href="#s:50"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
All these proofs can be done just by <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="NatList.test_count1" class="idref" href="#NatList.test_count1"><span class="id" title="definition">test_count1</span></a>:              <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 1 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_count2" class="idref" href="#NatList.test_count2"><span class="id" title="definition">test_count2</span></a>:              <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 6 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
Multiset <span class="inlinecode"><span class="id" title="var">sum</span></span> is similar to set <span class="inlinecode"><span class="id" title="var">union</span></span>: <span class="inlinecode"><span class="id" title="var">sum</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode"><span class="id" title="var">b</span></span> contains all
    the elements of <span class="inlinecode"><span class="id" title="var">a</span></span> and of <span class="inlinecode"><span class="id" title="var">b</span></span>.  (Mathematicians usually define
    <span class="inlinecode"><span class="id" title="var">union</span></span> on multisets a little bit differently -- using max instead
    of sum -- which is why we don't call this operation <span class="inlinecode"><span class="id" title="var">union</span></span>.)  For
    <span class="inlinecode"><span class="id" title="var">sum</span></span>, we're giving you a header that does not give explicit names
    to the arguments.  Moreover, it uses the keyword <span class="inlinecode"><span class="id" title="keyword">Definition</span></span>
    instead of <span class="inlinecode"><span class="id" title="keyword">Fixpoint</span></span>, so even if you had names for the arguments,
    you wouldn't be able to process them recursively.  The point of
    stating the question this way is to encourage you to think about
    whether <span class="inlinecode"><span class="id" title="var">sum</span></span> can be implemented in another way -- perhaps by
    using one or more functions that have already been defined.  
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.sum" class="idref" href="#NatList.sum"><span class="id" title="definition">sum</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_sum1" class="idref" href="#NatList.test_sum1"><span class="id" title="definition">test_sum1</span></a>:              <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 1 (<a class="idref" href="Lists.html#NatList.sum"><span class="id" title="axiom">sum</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.add" class="idref" href="#NatList.add"><span class="id" title="definition">add</span></a> (<a id="v:52" class="idref" href="#v:52"><span class="id" title="binder">v</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="s:53" class="idref" href="#s:53"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_add1" class="idref" href="#NatList.test_add1"><span class="id" title="definition">test_add1</span></a>:                <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 1 (<a class="idref" href="Lists.html#NatList.add"><span class="id" title="axiom">add</span></a> 1 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_add2" class="idref" href="#NatList.test_add2"><span class="id" title="definition">test_add2</span></a>:                <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.add"><span class="id" title="axiom">add</span></a> 1 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="NatList.member" class="idref" href="#NatList.member"><span class="id" title="definition">member</span></a> (<a id="v:54" class="idref" href="#v:54"><span class="id" title="binder">v</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="s:55" class="idref" href="#s:55"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_member1" class="idref" href="#NatList.test_member1"><span class="id" title="definition">test_member1</span></a>:             <a class="idref" href="Lists.html#NatList.member"><span class="id" title="axiom">member</span></a> 1 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_member2" class="idref" href="#NatList.test_member2"><span class="id" title="definition">test_member2</span></a>:             <a class="idref" href="Lists.html#NatList.member"><span class="id" title="axiom">member</span></a> 2 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab80"></a><h4 class="section">Exercise: 3 stars, standard, optional (bag_more_functions)</h4>
 Here are some more <span class="inlinecode"><span class="id" title="var">bag</span></span> functions for you to practice with. 
<div class="paragraph"> </div>

 When <span class="inlinecode"><span class="id" title="var">remove_one</span></span> is applied to a bag without the number to
    remove, it should return the same bag unchanged.  (This exercise
    is optional, but students following the advanced track will need
    to fill in the definition of <span class="inlinecode"><span class="id" title="var">remove_one</span></span> for a later
    exercise.) 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.remove_one" class="idref" href="#NatList.remove_one"><span class="id" title="definition">remove_one</span></a> (<a id="v:56" class="idref" href="#v:56"><span class="id" title="binder">v</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="s:57" class="idref" href="#s:57"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_one1" class="idref" href="#NatList.test_remove_one1"><span class="id" title="definition">test_remove_one1</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_one"><span class="id" title="axiom">remove_one</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_one2" class="idref" href="#NatList.test_remove_one2"><span class="id" title="definition">test_remove_one2</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_one"><span class="id" title="axiom">remove_one</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_one3" class="idref" href="#NatList.test_remove_one3"><span class="id" title="definition">test_remove_one3</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 4 (<a class="idref" href="Lists.html#NatList.remove_one"><span class="id" title="axiom">remove_one</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 2.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_one4" class="idref" href="#NatList.test_remove_one4"><span class="id" title="definition">test_remove_one4</span></a>:<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_one"><span class="id" title="axiom">remove_one</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="NatList.remove_all" class="idref" href="#NatList.remove_all"><span class="id" title="definition">remove_all</span></a> (<a id="v:59" class="idref" href="#v:59"><span class="id" title="binder">v</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="s:60" class="idref" href="#s:60"><span class="id" title="binder">s</span></a>:<a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_all1" class="idref" href="#NatList.test_remove_all1"><span class="id" title="definition">test_remove_all1</span></a>:  <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_all"><span class="id" title="axiom">remove_all</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_all2" class="idref" href="#NatList.test_remove_all2"><span class="id" title="definition">test_remove_all2</span></a>:  <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_all"><span class="id" title="axiom">remove_all</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_all3" class="idref" href="#NatList.test_remove_all3"><span class="id" title="definition">test_remove_all3</span></a>:  <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 4 (<a class="idref" href="Lists.html#NatList.remove_all"><span class="id" title="axiom">remove_all</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 2.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_remove_all4" class="idref" href="#NatList.test_remove_all4"><span class="id" title="definition">test_remove_all4</span></a>:  <a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 5 (<a class="idref" href="Lists.html#NatList.remove_all"><span class="id" title="axiom">remove_all</span></a> 5 <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="NatList.subset" class="idref" href="#NatList.subset"><span class="id" title="definition">subset</span></a> (<a id="s<sub>1</sub>:62" class="idref" href="#s<sub>1</sub>:62"><span class="id" title="binder">s<sub>1</sub></span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) (<a id="s<sub>2</sub>:63" class="idref" href="#s<sub>2</sub>:63"><span class="id" title="binder">s<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_subset1" class="idref" href="#NatList.test_subset1"><span class="id" title="definition">test_subset1</span></a>:              <a class="idref" href="Lists.html#NatList.subset"><span class="id" title="axiom">subset</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_subset2" class="idref" href="#NatList.test_subset2"><span class="id" title="definition">test_subset2</span></a>:              <a class="idref" href="Lists.html#NatList.subset"><span class="id" title="axiom">subset</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab81"></a><h4 class="section">Exercise: 2 stars, standard, especially useful (add_inc_count)</h4>
 Adding a value to a bag should increase the value's count by one.
    State that as a theorem and prove it. 
</div>
<div class="code">
<span class="comment">(*<br/>
Theorem&nbsp;bag_theorem&nbsp;:&nbsp;...<br/>
Proof.<br/>
&nbsp;&nbsp;...<br/>
Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="NatList.manual_grade_for_add_inc_count" class="idref" href="#NatList.manual_grade_for_add_inc_count"><span class="id" title="definition">manual_grade_for_add_inc_count</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab82"></a><h1 class="section">Reasoning About Lists</h1>

<div class="paragraph"> </div>

 As with numbers, simple facts about list-processing
    functions can sometimes be proved entirely by simplification.  For
    example, just the simplification performed by <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span> is
    enough for this theorem... 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.nil_app" class="idref" href="#NatList.nil_app"><span class="id" title="lemma">nil_app</span></a> : <span class="id" title="keyword">∀</span> <a id="l:65" class="idref" href="#l:65"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">[]</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l:65"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#l:65"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
...because the <span class="inlinecode">[]</span> is substituted into the
    "scrutinee" (the expression whose value is being "scrutinized" by
    the match) in the definition of <span class="inlinecode"><span class="id" title="var">app</span></span>, allowing the match itself
    to be simplified. 
<div class="paragraph"> </div>

 Also, as with numbers, it is sometimes helpful to perform case
    analysis on the possible shapes (empty or non-empty) of an unknown
    list. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.tl_length_pred" class="idref" href="#NatList.tl_length_pred"><span class="id" title="lemma">tl_length_pred</span></a> : <span class="id" title="keyword">∀</span> <a id="l:66" class="idref" href="#l:66"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#pred"><span class="id" title="abbreviation">pred</span></a> (<a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> <a class="idref" href="Lists.html#l:66"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Lists.html#NatList.tl"><span class="id" title="definition">tl</span></a> <a class="idref" href="Lists.html#l:66"><span class="id" title="variable">l</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">l</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">l</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n</span> <span class="id" title="var">l'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;nil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;cons&nbsp;n&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here, the <span class="inlinecode"><span class="id" title="var">nil</span></span> case works because we've chosen to define
    <span class="inlinecode"><span class="id" title="var">tl</span></span> <span class="inlinecode"><span class="id" title="var">nil</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">nil</span></span>. Notice that the <span class="inlinecode"><span class="id" title="keyword">as</span></span> annotation on the <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>
    tactic here introduces two names, <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">l'</span></span>, corresponding to
    the fact that the <span class="inlinecode"><span class="id" title="var">cons</span></span> constructor for lists takes two
    arguments (the head and tail of the list it is constructing). 
<div class="paragraph"> </div>

 Usually, though, interesting theorems about lists require
    induction for their proofs.  We'll see how to do this next. 
<div class="paragraph"> </div>

 (Micro-Sermon: As we get deeper into this material, simply
    <i>reading</i> proof scripts will not get you very far!  It is
    important to step through the details of each one using Coq and
    think about what each step achieves.  Otherwise it is more or less
    guaranteed that the exercises will make no sense when you get to
    them.  'Nuff said.) 
</div>

<div class="doc">
<a id="lab83"></a><h2 class="section">Induction on Lists</h2>

<div class="paragraph"> </div>

 Proofs by induction over datatypes like <span class="inlinecode"><span class="id" title="var">natlist</span></span> are a
    little less familiar than standard natural number induction, but
    the idea is equally simple.  Each <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span> declaration defines
    a set of data values that can be built up using the declared
    constructors.  For example, a boolean can be either <span class="inlinecode"><span class="id" title="var">true</span></span> or
    <span class="inlinecode"><span class="id" title="var">false</span></span>; a number can be either <span class="inlinecode"><span class="id" title="var">O</span></span> or <span class="inlinecode"><span class="id" title="var">S</span></span> applied to another
    number; and a list can be either <span class="inlinecode"><span class="id" title="var">nil</span></span> or <span class="inlinecode"><span class="id" title="var">cons</span></span> applied to a
    number and a list.   Moreover, applications of the declared
    constructors to one another are the <i>only</i> possible shapes
    that elements of an inductively defined set can have.

<div class="paragraph"> </div>

    This last fact directly gives rise to a way of reasoning about
    inductively defined sets: a number is either <span class="inlinecode"><span class="id" title="var">O</span></span> or else it is <span class="inlinecode"><span class="id" title="var">S</span></span>
    applied to some <i>smaller</i> number; a list is either <span class="inlinecode"><span class="id" title="var">nil</span></span> or else
    it is <span class="inlinecode"><span class="id" title="var">cons</span></span> applied to some number and some <i>smaller</i> list;
    etc. So, if we have in mind some proposition <span class="inlinecode"><span class="id" title="var">P</span></span> that mentions a
    list <span class="inlinecode"><span class="id" title="var">l</span></span> and we want to argue that <span class="inlinecode"><span class="id" title="var">P</span></span> holds for <i>all</i> lists, we
    can reason as follows:

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, show that <span class="inlinecode"><span class="id" title="var">P</span></span> is true of <span class="inlinecode"><span class="id" title="var">l</span></span> when <span class="inlinecode"><span class="id" title="var">l</span></span> is <span class="inlinecode"><span class="id" title="var">nil</span></span>.

<div class="paragraph"> </div>


</li>
<li> Then show that <span class="inlinecode"><span class="id" title="var">P</span></span> is true of <span class="inlinecode"><span class="id" title="var">l</span></span> when <span class="inlinecode"><span class="id" title="var">l</span></span> is <span class="inlinecode"><span class="id" title="var">cons</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode"><span class="id" title="var">l'</span></span> for
        some number <span class="inlinecode"><span class="id" title="var">n</span></span> and some smaller list <span class="inlinecode"><span class="id" title="var">l'</span></span>, assuming that <span class="inlinecode"><span class="id" title="var">P</span></span>
        is true for <span class="inlinecode"><span class="id" title="var">l'</span></span>.

</li>
</ul>

<div class="paragraph"> </div>

    Since larger lists can always be broken down into smaller ones,
    eventually reaching <span class="inlinecode"><span class="id" title="var">nil</span></span>, these two arguments together establish
    the truth of <span class="inlinecode"><span class="id" title="var">P</span></span> for all lists <span class="inlinecode"><span class="id" title="var">l</span></span>.  Here's a concrete example: 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.app_assoc" class="idref" href="#NatList.app_assoc"><span class="id" title="lemma">app_assoc</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:67" class="idref" href="#l<sub>1</sub>:67"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:68" class="idref" href="#l<sub>2</sub>:68"><span class="id" title="binder">l<sub>2</sub></span></a> <a id="l<sub>3</sub>:69" class="idref" href="#l<sub>3</sub>:69"><span class="id" title="binder">l<sub>3</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#l<sub>1</sub>:67"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:68"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>3</sub>:69"><span class="id" title="variable">l<sub>3</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:67"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#l<sub>2</sub>:68"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>3</sub>:69"><span class="id" title="variable">l<sub>3</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">l<sub>1</sub></span> <span class="id" title="var">l<sub>2</sub></span> <span class="id" title="var">l<sub>3</sub></span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">l<sub>1</sub></span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n</span> <span class="id" title="var">l<sub>1</sub>'</span> <span class="id" title="var">IHl1'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l<sub>1</sub>&nbsp;=&nbsp;nil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l<sub>1</sub>&nbsp;=&nbsp;cons&nbsp;n&nbsp;l<sub>1</sub>'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">IHl1'</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Notice that, as when doing induction on natural numbers, the
    <span class="inlinecode"><span class="id" title="keyword">as</span>...</span> clause provided to the <span class="inlinecode"><span class="id" title="tactic">induction</span></span> tactic gives a name to
    the induction hypothesis corresponding to the smaller list <span class="inlinecode"><span class="id" title="var">l<sub>1</sub>'</span></span>
    in the <span class="inlinecode"><span class="id" title="var">cons</span></span> case.

<div class="paragraph"> </div>

    Once again, this Coq proof is not especially illuminating as a
    static document -- it is easy to see what's going on if you are
    reading the proof in an interactive Coq session and you can see
    the current goal and context at each point, but this state is not
    visible in the written-down parts of the Coq proof.  So a
    natural-language proof -- one written for human readers -- will
    need to include more explicit signposts; in particular, it will
    help the reader stay oriented if we remind them exactly what the
    induction hypothesis is in the second case. 
<div class="paragraph"> </div>

 For comparison, here is an informal proof of the same theorem. 
<div class="paragraph"> </div>

 <i>Theorem</i>: For all lists <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span></span>, and <span class="inlinecode"><span class="id" title="var">l<sub>3</sub></span></span>,
   <span class="inlinecode">(<span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span>)</span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" title="var">l<sub>3</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode">(<span class="id" title="var">l<sub>2</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" title="var">l<sub>3</sub></span>)</span>.

<div class="paragraph"> </div>

   <i>Proof</i>: By induction on <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, suppose <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">[]</span>.  We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;([] ++ <span class="id" title="var">l<sub>2</sub></span>) ++ <span class="id" title="var">l<sub>3</sub></span> = [] ++ (<span class="id" title="var">l<sub>2</sub></span> ++ <span class="id" title="var">l<sub>3</sub></span>),
</span>     which follows directly from the definition of <span class="inlinecode">++</span>.

<div class="paragraph"> </div>


</li>
<li> Next, suppose <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span>::<span class="id" title="var">l<sub>1</sub>'</span></span>, with
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">l<sub>1</sub>'</span> ++ <span class="id" title="var">l<sub>2</sub></span>) ++ <span class="id" title="var">l<sub>3</sub></span> = <span class="id" title="var">l<sub>1</sub>'</span> ++ (<span class="id" title="var">l<sub>2</sub></span> ++ <span class="id" title="var">l<sub>3</sub></span>)
</span>     (the induction hypothesis). We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id" title="var">n</span> :: <span class="id" title="var">l<sub>1</sub>'</span>) ++ <span class="id" title="var">l<sub>2</sub></span>) ++ <span class="id" title="var">l<sub>3</sub></span> = (<span class="id" title="var">n</span> :: <span class="id" title="var">l<sub>1</sub>'</span>) ++ (<span class="id" title="var">l<sub>2</sub></span> ++ <span class="id" title="var">l<sub>3</sub></span>).
</span>     By the definition of <span class="inlinecode">++</span>, this follows from
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">n</span> :: ((<span class="id" title="var">l<sub>1</sub>'</span> ++ <span class="id" title="var">l<sub>2</sub></span>) ++ <span class="id" title="var">l<sub>3</sub></span>) = <span class="id" title="var">n</span> :: (<span class="id" title="var">l<sub>1</sub>'</span> ++ (<span class="id" title="var">l<sub>2</sub></span> ++ <span class="id" title="var">l<sub>3</sub></span>)),
</span>     which is immediate from the induction hypothesis.  <font size=-2>&#9744;</font> 
</li>
</ul>

<div class="paragraph"> </div>

<a id="lab84"></a><h3 class="section">Reversing a List</h3>

<div class="paragraph"> </div>

 For a slightly more involved example of inductive proof over
    lists, suppose we use <span class="inlinecode"><span class="id" title="var">app</span></span> to define a list-reversing
    function <span class="inlinecode"><span class="id" title="var">rev</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.rev" class="idref" href="#NatList.rev"><span class="id" title="definition">rev</span></a> (<a id="l:70" class="idref" href="#l:70"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:70"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>    ⇒ <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">h</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒ <a class="idref" href="Lists.html#rev:71"><span class="id" title="definition">rev</span></a> <span class="id" title="var">t</span> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a><span class="id" title="var">h</span><a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_rev1" class="idref" href="#NatList.test_rev1"><span class="id" title="definition">test_rev1</span></a>:            <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_rev2" class="idref" href="#NatList.test_rev2"><span class="id" title="definition">test_rev2</span></a>:            <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
For something a bit more challenging than the proofs
    we've seen so far, let's prove that reversing a list does not
    change its length.  Our first attempt gets stuck in the successor
    case... 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.rev_length_firsttry" class="idref" href="#NatList.rev_length_firsttry"><span class="id" title="lemma">rev_length_firsttry</span></a> : <span class="id" title="keyword">∀</span> <a id="l:73" class="idref" href="#l:73"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l:73"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> <a class="idref" href="Lists.html#l:73"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">l</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">l</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n</span> <span class="id" title="var">l'</span> <span class="id" title="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;nil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;n&nbsp;::&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;This&nbsp;is&nbsp;the&nbsp;tricky&nbsp;case.&nbsp;&nbsp;Let's&nbsp;begin&nbsp;as&nbsp;usual<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;by&nbsp;simplifying.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Now&nbsp;we&nbsp;seem&nbsp;to&nbsp;be&nbsp;stuck:&nbsp;the&nbsp;goal&nbsp;is&nbsp;an&nbsp;equality<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;involving&nbsp;<span class="inlinecode">++</span>,&nbsp;but&nbsp;we&nbsp;don't&nbsp;have&nbsp;any&nbsp;useful&nbsp;equations<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in&nbsp;either&nbsp;the&nbsp;immediate&nbsp;context&nbsp;or&nbsp;in&nbsp;the&nbsp;global<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;environment!&nbsp;&nbsp;We&nbsp;can&nbsp;make&nbsp;a&nbsp;little&nbsp;progress&nbsp;by&nbsp;using<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;IH&nbsp;to&nbsp;rewrite&nbsp;the&nbsp;goal...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> &lt;- <span class="id" title="var">IHl'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;...&nbsp;but&nbsp;now&nbsp;we&nbsp;can't&nbsp;go&nbsp;any&nbsp;further.&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
So let's take the equation relating <span class="inlinecode">++</span> and <span class="inlinecode"><span class="id" title="var">length</span></span> that
    would have enabled us to make progress at the point where we got
    stuck and state it as a separate lemma. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.app_length" class="idref" href="#NatList.app_length"><span class="id" title="lemma">app_length</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:74" class="idref" href="#l<sub>1</sub>:74"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:75" class="idref" href="#l<sub>2</sub>:75"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Lists.html#l<sub>1</sub>:74"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:75"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:74"><span class="id" title="variable">l<sub>1</sub></span></a><a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:75"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">l<sub>1</sub></span> <span class="id" title="var">l<sub>2</sub></span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">l<sub>1</sub></span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n</span> <span class="id" title="var">l<sub>1</sub>'</span> <span class="id" title="var">IHl1'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l<sub>1</sub>&nbsp;=&nbsp;nil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l<sub>1</sub>&nbsp;=&nbsp;cons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">IHl1'</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Note that, to make the lemma as general as possible, we
    quantify over <i>all</i> <span class="inlinecode"><span class="id" title="var">natlist</span></span>s, not just those that result from an
    application of <span class="inlinecode"><span class="id" title="var">rev</span></span>.  This should seem natural, because the truth
    of the goal clearly doesn't depend on the list having been
    reversed.  Moreover, it is easier to prove the more general
    property. 
<div class="paragraph"> </div>

 Now we can complete the original proof. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.rev_length" class="idref" href="#NatList.rev_length"><span class="id" title="lemma">rev_length</span></a> : <span class="id" title="keyword">∀</span> <a id="l:76" class="idref" href="#l:76"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> (<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l:76"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.length"><span class="id" title="definition">length</span></a> <a class="idref" href="Lists.html#l:76"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">l</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">l</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n</span> <span class="id" title="var">l'</span> <span class="id" title="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;nil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;cons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> → <a class="idref" href="Lists.html#NatList.app_length"><span class="id" title="lemma">app_length</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">IHl'</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#add_comm"><span class="id" title="axiom">add_comm</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
For comparison, here are informal proofs of these two theorems:

<div class="paragraph"> </div>

    <i>Theorem</i>: For all lists <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span></span>,
       <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode">(<span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: By induction on <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, suppose <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">[]</span>.  We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> ([] ++ <span class="id" title="var">l<sub>2</sub></span>) = <span class="id" title="var">length</span> [] + <span class="id" title="var">length</span> <span class="id" title="var">l<sub>2</sub></span>,
</span>      which follows directly from the definitions of
      <span class="inlinecode"><span class="id" title="var">length</span></span>, <span class="inlinecode">++</span>, and <span class="inlinecode"><span class="id" title="var">plus</span></span>.

<div class="paragraph"> </div>


</li>
<li> Next, suppose <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span>::<span class="id" title="var">l<sub>1</sub>'</span></span>, with
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> (<span class="id" title="var">l<sub>1</sub>'</span> ++ <span class="id" title="var">l<sub>2</sub></span>) = <span class="id" title="var">length</span> <span class="id" title="var">l<sub>1</sub>'</span> + <span class="id" title="var">length</span> <span class="id" title="var">l<sub>2</sub></span>.
</span>      We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> ((<span class="id" title="var">n</span>::<span class="id" title="var">l<sub>1</sub>'</span>) ++ <span class="id" title="var">l<sub>2</sub></span>) = <span class="id" title="var">length</span> (<span class="id" title="var">n</span>::<span class="id" title="var">l<sub>1</sub>'</span>) + <span class="id" title="var">length</span> <span class="id" title="var">l<sub>2</sub></span>.
</span>      This follows directly from the definitions of <span class="inlinecode"><span class="id" title="var">length</span></span> and <span class="inlinecode">++</span>
      together with the induction hypothesis. <font size=-2>&#9744;</font> 
</li>
</ul>

<div class="paragraph"> </div>

 <i>Theorem</i>: For all lists <span class="inlinecode"><span class="id" title="var">l</span></span>, <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode">(<span class="id" title="var">rev</span></span> <span class="inlinecode"><span class="id" title="var">l</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode"><span class="id" title="var">l</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: By induction on <span class="inlinecode"><span class="id" title="var">l</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, suppose <span class="inlinecode"><span class="id" title="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode">[]</span>.  We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> (<span class="id" title="var">rev</span> []) = <span class="id" title="var">length</span> [],
</span>        which follows directly from the definitions of <span class="inlinecode"><span class="id" title="var">length</span></span>
        and <span class="inlinecode"><span class="id" title="var">rev</span></span>.

<div class="paragraph"> </div>


</li>
<li> Next, suppose <span class="inlinecode"><span class="id" title="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span>::<span class="id" title="var">l'</span></span>, with
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> (<span class="id" title="var">rev</span> <span class="id" title="var">l'</span>) = <span class="id" title="var">length</span> <span class="id" title="var">l'</span>.
</span>        We must show
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> (<span class="id" title="var">rev</span> (<span class="id" title="var">n</span> :: <span class="id" title="var">l'</span>)) = <span class="id" title="var">length</span> (<span class="id" title="var">n</span> :: <span class="id" title="var">l'</span>).
</span>        By the definition of <span class="inlinecode"><span class="id" title="var">rev</span></span>, this follows from
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> ((<span class="id" title="var">rev</span> <span class="id" title="var">l'</span>) ++ [<span class="id" title="var">n</span>]) = <span class="id" title="var">S</span> (<span class="id" title="var">length</span> <span class="id" title="var">l'</span>)
</span>        which, by the previous lemma, is the same as
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">length</span> (<span class="id" title="var">rev</span> <span class="id" title="var">l'</span>) + <span class="id" title="var">length</span> [<span class="id" title="var">n</span>] = <span class="id" title="var">S</span> (<span class="id" title="var">length</span> <span class="id" title="var">l'</span>).
</span>        This follows directly from the induction hypothesis and the
        definition of <span class="inlinecode"><span class="id" title="var">length</span></span>. <font size=-2>&#9744;</font> 
</li>
</ul>

<div class="paragraph"> </div>

 The style of these proofs is rather longwinded and pedantic.
    After reading a couple like this, we might find it easier to
    follow proofs that give fewer details (which we can easily work
    out in our own minds or on scratch paper if necessary) and just
    highlight the non-obvious steps.  In this more compressed style,
    the above proof might look like this: 
<div class="paragraph"> </div>

 <i>Theorem</i>: For all lists <span class="inlinecode"><span class="id" title="var">l</span></span>, <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode">(<span class="id" title="var">rev</span></span> <span class="inlinecode"><span class="id" title="var">l</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode"><span class="id" title="var">l</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: First, observe that <span class="inlinecode"><span class="id" title="var">length</span></span> <span class="inlinecode">(<span class="id" title="var">l</span></span> <span class="inlinecode">++</span> <span class="inlinecode">[<span class="id" title="var">n</span>])</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">length</span></span> <span class="inlinecode"><span class="id" title="var">l</span>)</span>
     for any <span class="inlinecode"><span class="id" title="var">l</span></span>, by a straightforward induction on <span class="inlinecode"><span class="id" title="var">l</span></span>.  The main
     property again follows by induction on <span class="inlinecode"><span class="id" title="var">l</span></span>, using the observation
     together with the induction hypothesis in the case where <span class="inlinecode"><span class="id" title="var">l</span></span> <span class="inlinecode">=</span>
     <span class="inlinecode"><span class="id" title="var">n'</span>::<span class="id" title="var">l'</span></span>. <font size=-2>&#9744;</font> 
<div class="paragraph"> </div>

 Which style is preferable in a given situation depends on
    the sophistication of the expected audience and how similar the
    proof at hand is to ones that they will already be familiar with.
    The more pedantic style is a good default for our present
    purposes. 
</div>

<div class="doc">
<a id="lab85"></a><h2 class="section"><span class="inlinecode"><span class="id" title="keyword">Search</span></span></h2>

<div class="paragraph"> </div>

 We've seen that proofs can make use of other theorems we've
    already proved, e.g., using <span class="inlinecode"><span class="id" title="tactic">rewrite</span></span>.  But in order to refer to a
    theorem, we need to know its name!  Indeed, it is often hard even
    to remember what theorems have been proven, much less what they
    are called.

<div class="paragraph"> </div>

    Coq's <span class="inlinecode"><span class="id" title="keyword">Search</span></span> command is quite helpful with this.  Let's say
    you've forgotten the name of a theorem about <span class="inlinecode"><span class="id" title="var">rev</span></span>.  The command
    <span class="inlinecode"><span class="id" title="keyword">Search</span></span> <span class="inlinecode"><span class="id" title="var">rev</span></span> will cause Coq to display a list of all theorems
    involving <span class="inlinecode"><span class="id" title="var">rev</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Search</span> <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a>.<br/>
</div>

<div class="doc">
Or say you've forgotten the name of the theorem showing that plus
    is commutative.  You can use a pattern to search for all theorems
    involving the equality of two additions. 
</div>
<div class="code">

<span class="id" title="keyword">Search</span> (<span class="id" title="var">_</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">_</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">_</span>).<br/>
</div>

<div class="doc">
You'll see a lot of results there, nearly all of them from the
    standard library.  To restrict the results, you can search inside
    a particular module: 
</div>
<div class="code">

<span class="id" title="keyword">Search</span> (<span class="id" title="var">_</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">_</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">inside</span> <span class="id" title="keyword">Induction</span>.<br/>
</div>

<div class="doc">
You can also make the search more precise by using variables in
    the search pattern instead of wildcards: 
</div>
<div class="code">

<span class="id" title="keyword">Search</span> (?<span class="id" title="var">x</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> ?<span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> ?<span class="id" title="var">y</span> <a class="idref" href="Basics.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> ?<span class="id" title="var">x</span>).<br/>
</div>

<div class="doc">
The question mark in front of the variable is needed to indicate
    that it is a variable in the search pattern, rather than a
    variable that is expected to be in scope currently. 
<div class="paragraph"> </div>

 Keep <span class="inlinecode"><span class="id" title="keyword">Search</span></span> in mind as you do the following exercises and
    throughout the rest of the book; it can save you a lot of time!

<div class="paragraph"> </div>

    Your IDE likely has its own functionality to help with searching.
    For example, in ProofGeneral, you can run <span class="inlinecode"><span class="id" title="keyword">Search</span></span> with <span class="inlinecode"><span class="id" title="var">C</span>-<span class="id" title="var">c</span></span> <span class="inlinecode"><span class="id" title="var">C</span>-<span class="id" title="var">a</span></span>
    <span class="inlinecode"><span class="id" title="var">C</span>-<span class="id" title="var">a</span></span>, and paste its response into your buffer with <span class="inlinecode"><span class="id" title="var">C</span>-<span class="id" title="var">c</span></span> <span class="inlinecode"><span class="id" title="var">C</span>-;</span>. 
</div>

<div class="doc">
<a id="lab86"></a><h2 class="section">List Exercises, Part 1</h2>

<div class="paragraph"> </div>

<a id="lab87"></a><h4 class="section">Exercise: 3 stars, standard (list_exercises)</h4>
 More practice with lists: 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.app_nil_r" class="idref" href="#NatList.app_nil_r"><span class="id" title="lemma">app_nil_r</span></a> : <span class="id" title="keyword">∀</span> <a id="l:77" class="idref" href="#l:77"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#l:77"><span class="id" title="variable">l</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#l:77"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="NatList.rev_app_distr" class="idref" href="#NatList.rev_app_distr"><span class="id" title="lemma">rev_app_distr</span></a>: <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:78" class="idref" href="#l<sub>1</sub>:78"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:79" class="idref" href="#l<sub>2</sub>:79"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Lists.html#l<sub>1</sub>:78"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:79"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:79"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:78"><span class="id" title="variable">l<sub>1</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="NatList.rev_involutive" class="idref" href="#NatList.rev_involutive"><span class="id" title="lemma">rev_involutive</span></a> : <span class="id" title="keyword">∀</span> <a id="l:80" class="idref" href="#l:80"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> (<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l:80"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#l:80"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
There is a short solution to the next one.  If you find yourself
    getting tangled up, step back and try to look for a simpler
    way. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.app_assoc4" class="idref" href="#NatList.app_assoc4"><span class="id" title="lemma">app_assoc4</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:81" class="idref" href="#l<sub>1</sub>:81"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:82" class="idref" href="#l<sub>2</sub>:82"><span class="id" title="binder">l<sub>2</sub></span></a> <a id="l<sub>3</sub>:83" class="idref" href="#l<sub>3</sub>:83"><span class="id" title="binder">l<sub>3</sub></span></a> <a id="l<sub>4</sub>:84" class="idref" href="#l<sub>4</sub>:84"><span class="id" title="binder">l<sub>4</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#l<sub>1</sub>:81"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#l<sub>2</sub>:82"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#l<sub>3</sub>:83"><span class="id" title="variable">l<sub>3</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>4</sub>:84"><span class="id" title="variable">l<sub>4</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">))</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">((</span></a><a class="idref" href="Lists.html#l<sub>1</sub>:81"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:82"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>3</sub>:83"><span class="id" title="variable">l<sub>3</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>4</sub>:84"><span class="id" title="variable">l<sub>4</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
An exercise about your implementation of <span class="inlinecode"><span class="id" title="var">nonzeros</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="NatList.nonzeros_app" class="idref" href="#NatList.nonzeros_app"><span class="id" title="lemma">nonzeros_app</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:85" class="idref" href="#l<sub>1</sub>:85"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:86" class="idref" href="#l<sub>2</sub>:86"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.nonzeros"><span class="id" title="axiom">nonzeros</span></a> (<a class="idref" href="Lists.html#l<sub>1</sub>:85"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:86"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.nonzeros"><span class="id" title="axiom">nonzeros</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:85"><span class="id" title="variable">l<sub>1</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.nonzeros"><span class="id" title="axiom">nonzeros</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:86"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Lists.html#9051c98c6b1a5a76d335ab187bb449a<sub>6</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab88"></a><h4 class="section">Exercise: 2 stars, standard (eqblist)</h4>
 Fill in the definition of <span class="inlinecode"><span class="id" title="var">eqblist</span></span>, which compares
    lists of numbers for equality.  Prove that <span class="inlinecode"><span class="id" title="var">eqblist</span></span> <span class="inlinecode"><span class="id" title="var">l</span></span> <span class="inlinecode"><span class="id" title="var">l</span></span>
    yields <span class="inlinecode"><span class="id" title="var">true</span></span> for every list <span class="inlinecode"><span class="id" title="var">l</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.eqblist" class="idref" href="#NatList.eqblist"><span class="id" title="definition">eqblist</span></a> (<a id="l<sub>1</sub>:87" class="idref" href="#l<sub>1</sub>:87"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:88" class="idref" href="#l<sub>2</sub>:88"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_eqblist1" class="idref" href="#NatList.test_eqblist1"><span class="id" title="definition">test_eqblist1</span></a> :<br/>
&nbsp;&nbsp;(<a class="idref" href="Lists.html#NatList.eqblist"><span class="id" title="axiom">eqblist</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>).<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_eqblist2" class="idref" href="#NatList.test_eqblist2"><span class="id" title="definition">test_eqblist2</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.eqblist"><span class="id" title="axiom">eqblist</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_eqblist3" class="idref" href="#NatList.test_eqblist3"><span class="id" title="definition">test_eqblist3</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.eqblist"><span class="id" title="axiom">eqblist</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>3<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>2<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="NatList.eqblist_refl" class="idref" href="#NatList.eqblist_refl"><span class="id" title="lemma">eqblist_refl</span></a> : <span class="id" title="keyword">∀</span> <a id="l:90" class="idref" href="#l:90"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.eqblist"><span class="id" title="axiom">eqblist</span></a> <a class="idref" href="Lists.html#l:90"><span class="id" title="variable">l</span></a> <a class="idref" href="Lists.html#l:90"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab89"></a><h2 class="section">List Exercises, Part 2</h2>

<div class="paragraph"> </div>

 Here are a couple of little theorems to prove about your
    definitions about bags above. 
<div class="paragraph"> </div>

<a id="lab90"></a><h4 class="section">Exercise: 1 star, standard (count_member_nonzero)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="NatList.count_member_nonzero" class="idref" href="#NatList.count_member_nonzero"><span class="id" title="lemma">count_member_nonzero</span></a> : <span class="id" title="keyword">∀</span> (<a id="s:91" class="idref" href="#s:91"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>),<br/>
&nbsp;&nbsp;1 <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 1 (1 <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Lists.html#s:91"><span class="id" title="variable">s</span></a>)<a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The following lemma about <span class="inlinecode"><span class="id" title="var">leb</span></span> might help you in the next
    exercise (it will also be useful in later chapters). 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.leb_n_Sn" class="idref" href="#NatList.leb_n_Sn"><span class="id" title="lemma">leb_n_Sn</span></a> : <span class="id" title="keyword">∀</span> <a id="n:92" class="idref" href="#n:92"><span class="id" title="binder">n</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#n:92"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Lists.html#n:92"><span class="id" title="variable">n</span></a><a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span> <span class="id" title="var">IHn'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S&nbsp;n'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHn'</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Before doing the next exercise, make sure you've filled in the
   definition of <span class="inlinecode"><span class="id" title="var">remove_one</span></span> above. <a id="lab91"></a><h4 class="section">Exercise: 3 stars, advanced (remove_does_not_increase_count)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="NatList.remove_does_not_increase_count" class="idref" href="#NatList.remove_does_not_increase_count"><span class="id" title="lemma">remove_does_not_increase_count</span></a>: <span class="id" title="keyword">∀</span> (<a id="s:93" class="idref" href="#s:93"><span class="id" title="binder">s</span></a> : <a class="idref" href="Lists.html#NatList.bag"><span class="id" title="definition">bag</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 0 (<a class="idref" href="Lists.html#NatList.remove_one"><span class="id" title="axiom">remove_one</span></a> 0 <a class="idref" href="Lists.html#s:93"><span class="id" title="variable">s</span></a>)<a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Lists.html#NatList.count"><span class="id" title="axiom">count</span></a> 0 <a class="idref" href="Lists.html#s:93"><span class="id" title="variable">s</span></a><a class="idref" href="Basics.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab92"></a><h4 class="section">Exercise: 3 stars, standard, optional (bag_count_sum)</h4>
 Write down an interesting theorem <span class="inlinecode"><span class="id" title="var">bag_count_sum</span></span> about bags
    involving the functions <span class="inlinecode"><span class="id" title="var">count</span></span> and <span class="inlinecode"><span class="id" title="var">sum</span></span>, and prove it using
    Coq.  (You may find that the difficulty of the proof depends on
    how you defined <span class="inlinecode"><span class="id" title="var">count</span></span>!  Hint: If you defined <span class="inlinecode"><span class="id" title="var">count</span></span> using
    <span class="inlinecode">=?</span> you may find it useful to know that <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> works on
    arbitrary expressions, not just simple identifiers.)

</div>
<div class="code">
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab93"></a><h4 class="section">Exercise: 4 stars, advanced (rev_injective)</h4>
 Prove that the <span class="inlinecode"><span class="id" title="var">rev</span></span> function is injective. There is a hard way
    and an easy way to do this. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.rev_injective" class="idref" href="#NatList.rev_injective"><span class="id" title="lemma">rev_injective</span></a> : <span class="id" title="keyword">∀</span> (<a id="l<sub>1</sub>:94" class="idref" href="#l<sub>1</sub>:94"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:95" class="idref" href="#l<sub>2</sub>:95"><span class="id" title="binder">l<sub>2</sub></span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:94"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:95"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Lists.html#l<sub>1</sub>:94"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#l<sub>2</sub>:95"><span class="id" title="variable">l<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab94"></a><h1 class="section">Options</h1>

<div class="paragraph"> </div>

 Suppose we want to write a function that returns the <span class="inlinecode"><span class="id" title="var">n</span></span>th
    element of some list.  If we give it type <span class="inlinecode"><span class="id" title="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">natlist</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">nat</span></span>,
    then we'll have to choose some number to return when the list is
    too short... 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.nth_bad" class="idref" href="#NatList.nth_bad"><span class="id" title="definition">nth_bad</span></a> (<a id="l:96" class="idref" href="#l:96"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) (<a id="n:97" class="idref" href="#n:97"><span class="id" title="binder">n</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:96"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> ⇒ 42<br/>
&nbsp;&nbsp;| <span class="id" title="var">a</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">l'</span> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#n:97"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| 0 ⇒ <span class="id" title="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Lists.html#nth_bad:98"><span class="id" title="definition">nth_bad</span></a> <span class="id" title="var">l'</span> <span class="id" title="var">n'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
This solution is not so good: If <span class="inlinecode"><span class="id" title="var">nth_bad</span></span> returns <span class="inlinecode">42</span>, we
    can't tell whether that value actually appears on the input
    without further processing. A better alternative is to change the
    return type of <span class="inlinecode"><span class="id" title="var">nth_bad</span></span> to include an error value as a possible
    outcome. We call this type <span class="inlinecode"><span class="id" title="var">natoption</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="NatList.natoption" class="idref" href="#NatList.natoption"><span class="id" title="inductive">natoption</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="NatList.Some" class="idref" href="#NatList.Some"><span class="id" title="constructor">Some</span></a> (<a id="n:103" class="idref" href="#n:103"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;| <a id="NatList.None" class="idref" href="#NatList.None"><span class="id" title="constructor">None</span></a>.<br/>
</div>

<div class="doc">
We can then change the above definition of <span class="inlinecode"><span class="id" title="var">nth_bad</span></span> to
    return <span class="inlinecode"><span class="id" title="var">None</span></span> when the list is too short and <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> when the
    list has enough members and <span class="inlinecode"><span class="id" title="var">a</span></span> appears at position <span class="inlinecode"><span class="id" title="var">n</span></span>. We call
    this new function <span class="inlinecode"><span class="id" title="var">nth_error</span></span> to indicate that it may result in an
    error. As we see here, constructors of inductive definitions can
    be capitalized. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="NatList.nth_error" class="idref" href="#NatList.nth_error"><span class="id" title="definition">nth_error</span></a> (<a id="l:104" class="idref" href="#l:104"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) (<a id="n:105" class="idref" href="#n:105"><span class="id" title="binder">n</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Lists.html#NatList.natoption"><span class="id" title="inductive">natoption</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#l:104"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.nil"><span class="id" title="constructor">nil</span></a> ⇒ <a class="idref" href="Lists.html#NatList.None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;| <span class="id" title="var">a</span> <a class="idref" href="Lists.html#NatList.:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">l'</span> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#n:105"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Lists.html#nth_error:106"><span class="id" title="definition">nth_error</span></a> <span class="id" title="var">l'</span> <span class="id" title="var">n'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_nth_error1" class="idref" href="#NatList.test_nth_error1"><span class="id" title="definition">test_nth_error1</span></a> : <a class="idref" href="Lists.html#NatList.nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>7<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> 4.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="NatList.test_nth_error2" class="idref" href="#NatList.test_nth_error2"><span class="id" title="definition">test_nth_error2</span></a> : <a class="idref" href="Lists.html#NatList.nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>7<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> 3 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> 7.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">Example</span> <a id="NatList.test_nth_error3" class="idref" href="#NatList.test_nth_error3"><span class="id" title="definition">test_nth_error3</span></a> : <a class="idref" href="Lists.html#NatList.nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>4<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>7<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> 9 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.None"><span class="id" title="constructor">None</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
(In the HTML version, the boilerplate proofs of these
    examples are elided.  Click on a box if you want to see one.)

<div class="paragraph"> </div>

 The function below pulls the <span class="inlinecode"><span class="id" title="var">nat</span></span> out of a <span class="inlinecode"><span class="id" title="var">natoption</span></span>, returning
    a supplied default in the <span class="inlinecode"><span class="id" title="var">None</span></span> case. 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.option_elim" class="idref" href="#NatList.option_elim"><span class="id" title="definition">option_elim</span></a> (<a id="d:109" class="idref" href="#d:109"><span class="id" title="binder">d</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="o:110" class="idref" href="#o:110"><span class="id" title="binder">o</span></a> : <a class="idref" href="Lists.html#NatList.natoption"><span class="id" title="inductive">natoption</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#o:110"><span class="id" title="variable">o</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">n'</span> ⇒ <span class="id" title="var">n'</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#NatList.None"><span class="id" title="constructor">None</span></a> ⇒ <a class="idref" href="Lists.html#d:109"><span class="id" title="variable">d</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab95"></a><h4 class="section">Exercise: 2 stars, standard (hd_error)</h4>
 Using the same idea, fix the <span class="inlinecode"><span class="id" title="var">hd</span></span> function from earlier so we don't
    have to pass a default element for the <span class="inlinecode"><span class="id" title="var">nil</span></span> case.  
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="NatList.hd_error" class="idref" href="#NatList.hd_error"><span class="id" title="definition">hd_error</span></a> (<a id="l:112" class="idref" href="#l:112"><span class="id" title="binder">l</span></a> : <a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) : <a class="idref" href="Lists.html#NatList.natoption"><span class="id" title="inductive">natoption</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_hd_error1" class="idref" href="#NatList.test_hd_error1"><span class="id" title="definition">test_hd_error1</span></a> : <a class="idref" href="Lists.html#NatList.hd_error"><span class="id" title="axiom">hd_error</span></a> <a class="idref" href="Lists.html#f5cee4f22b9033d1d704f9d537452cd<sub>0</sub>"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.None"><span class="id" title="constructor">None</span></a>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_hd_error2" class="idref" href="#NatList.test_hd_error2"><span class="id" title="definition">test_hd_error2</span></a> : <a class="idref" href="Lists.html#NatList.hd_error"><span class="id" title="axiom">hd_error</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>1<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> 1.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="NatList.test_hd_error3" class="idref" href="#NatList.test_hd_error3"><span class="id" title="definition">test_hd_error3</span></a> : <a class="idref" href="Lists.html#NatList.hd_error"><span class="id" title="axiom">hd_error</span></a> <a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">[</span></a>5<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">;</span></a>6<a class="idref" href="Lists.html#62815778618d6f51cd0f9ac90bf0e8be"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> 5.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab96"></a><h4 class="section">Exercise: 1 star, standard, optional (option_elim_hd)</h4>
 This exercise relates your new <span class="inlinecode"><span class="id" title="var">hd_error</span></span> to the old <span class="inlinecode"><span class="id" title="var">hd</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="NatList.option_elim_hd" class="idref" href="#NatList.option_elim_hd"><span class="id" title="lemma">option_elim_hd</span></a> : <span class="id" title="keyword">∀</span> (<a id="l:113" class="idref" href="#l:113"><span class="id" title="binder">l</span></a>:<a class="idref" href="Lists.html#NatList.natlist"><span class="id" title="inductive">natlist</span></a>) (<a id="default:114" class="idref" href="#default:114"><span class="id" title="binder">default</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#NatList.hd"><span class="id" title="definition">hd</span></a> <a class="idref" href="Lists.html#default:114"><span class="id" title="variable">default</span></a> <a class="idref" href="Lists.html#l:113"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.option_elim"><span class="id" title="definition">option_elim</span></a> <a class="idref" href="Lists.html#default:114"><span class="id" title="variable">default</span></a> (<a class="idref" href="Lists.html#NatList.hd_error"><span class="id" title="axiom">hd_error</span></a> <a class="idref" href="Lists.html#l:113"><span class="id" title="variable">l</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<span class="id" title="keyword">End</span> <a class="idref" href="Lists.html#NatList"><span class="id" title="module">NatList</span></a>.<br/>
</div>

<div class="doc">
<a id="lab97"></a><h1 class="section">Partial Maps</h1>

<div class="paragraph"> </div>

 As a final illustration of how data structures can be defined in
    Coq, here is a simple <i>partial map</i> data type, analogous to the
    map or dictionary data structures found in most programming
    languages. 
<div class="paragraph"> </div>

 First, we define a new inductive datatype <span class="inlinecode"><span class="id" title="var">id</span></span> to serve as the
    "keys" of our partial maps. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="id" class="idref" href="#id"><span class="id" title="inductive">id</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="Id" class="idref" href="#Id"><span class="id" title="constructor">Id</span></a> (<a id="n:117" class="idref" href="#n:117"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/>
</div>

<div class="doc">
Internally, an <span class="inlinecode"><span class="id" title="var">id</span></span> is just a number.  Introducing a separate type
    by wrapping each nat with the tag <span class="inlinecode"><span class="id" title="var">Id</span></span> makes definitions more
    readable and gives us more flexibility. 
<div class="paragraph"> </div>

 We'll also need an equality test for <span class="inlinecode"><span class="id" title="var">id</span></span>s: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="eqb_id" class="idref" href="#eqb_id"><span class="id" title="definition">eqb_id</span></a> (<a id="x<sub>1</sub>:118" class="idref" href="#x<sub>1</sub>:118"><span class="id" title="binder">x<sub>1</sub></span></a> <a id="x<sub>2</sub>:119" class="idref" href="#x<sub>2</sub>:119"><span class="id" title="binder">x<sub>2</sub></span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#x<sub>1</sub>:118"><span class="id" title="variable">x<sub>1</sub></span></a>, <a class="idref" href="Lists.html#x<sub>2</sub>:119"><span class="id" title="variable">x<sub>2</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#Id"><span class="id" title="constructor">Id</span></a> <span class="id" title="var">n<sub>1</sub></span>, <a class="idref" href="Lists.html#Id"><span class="id" title="constructor">Id</span></a> <span class="id" title="var">n<sub>2</sub></span> ⇒ <span class="id" title="var">n<sub>1</sub></span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <span class="id" title="var">n<sub>2</sub></span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab98"></a><h4 class="section">Exercise: 1 star, standard (eqb_id_refl)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="eqb_id_refl" class="idref" href="#eqb_id_refl"><span class="id" title="lemma">eqb_id_refl</span></a> : <span class="id" title="keyword">∀</span> <a id="x:122" class="idref" href="#x:122"><span class="id" title="binder">x</span></a>, <a class="idref" href="Lists.html#eqb_id"><span class="id" title="definition">eqb_id</span></a> <a class="idref" href="Lists.html#x:122"><span class="id" title="variable">x</span></a> <a class="idref" href="Lists.html#x:122"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 Now we define the type of partial maps: 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="PartialMap" class="idref" href="#PartialMap"><span class="id" title="module">PartialMap</span></a>.<br/>
<span class="id" title="keyword">Export</span> <span class="id" title="var">NatList</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="PartialMap.partial_map" class="idref" href="#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="PartialMap.empty" class="idref" href="#PartialMap.empty"><span class="id" title="constructor">empty</span></a><br/>
&nbsp;&nbsp;| <a id="PartialMap.record" class="idref" href="#PartialMap.record"><span class="id" title="constructor">record</span></a> (<a id="i:125" class="idref" href="#i:125"><span class="id" title="binder">i</span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) (<a id="v:126" class="idref" href="#v:126"><span class="id" title="binder">v</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="m:127" class="idref" href="#m:127"><span class="id" title="binder">m</span></a> : <a class="idref" href="Lists.html#partial_map:123"><span class="id" title="inductive">partial_map</span></a>).<br/>
</div>

<div class="doc">
This declaration can be read: "There are two ways to construct a
    <span class="inlinecode"><span class="id" title="var">partial_map</span></span>: either using the constructor <span class="inlinecode"><span class="id" title="var">empty</span></span> to represent an
    empty partial map, or applying the constructor <span class="inlinecode"><span class="id" title="var">record</span></span> to
    a key, a value, and an existing <span class="inlinecode"><span class="id" title="var">partial_map</span></span> to construct a
    <span class="inlinecode"><span class="id" title="var">partial_map</span></span> with an additional key-to-value mapping." 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="var">update</span></span> function overrides the entry for a given key in a
    partial map by shadowing it with a new one (or simply adds a new
    entry if the given key is not already present). 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="PartialMap.update" class="idref" href="#PartialMap.update"><span class="id" title="definition">update</span></a> (<a id="d:128" class="idref" href="#d:128"><span class="id" title="binder">d</span></a> : <a class="idref" href="Lists.html#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="x:129" class="idref" href="#x:129"><span class="id" title="binder">x</span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) (<a id="value:130" class="idref" href="#value:130"><span class="id" title="binder">value</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Lists.html#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="Lists.html#PartialMap.record"><span class="id" title="constructor">record</span></a> <a class="idref" href="Lists.html#x:129"><span class="id" title="variable">x</span></a> <a class="idref" href="Lists.html#value:130"><span class="id" title="variable">value</span></a> <a class="idref" href="Lists.html#d:128"><span class="id" title="variable">d</span></a>.<br/>
</div>

<div class="doc">
Last, the <span class="inlinecode"><span class="id" title="var">find</span></span> function searches a <span class="inlinecode"><span class="id" title="var">partial_map</span></span> for a given
    key.  It returns <span class="inlinecode"><span class="id" title="var">None</span></span> if the key was not found and <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">val</span></span> if
    the key was associated with <span class="inlinecode"><span class="id" title="var">val</span></span>. If the same key is mapped to
    multiple values, <span class="inlinecode"><span class="id" title="var">find</span></span> will return the first one it
    encounters. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="PartialMap.find" class="idref" href="#PartialMap.find"><span class="id" title="definition">find</span></a> (<a id="x:131" class="idref" href="#x:131"><span class="id" title="binder">x</span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) (<a id="d:132" class="idref" href="#d:132"><span class="id" title="binder">d</span></a> : <a class="idref" href="Lists.html#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a>) : <a class="idref" href="Lists.html#NatList.natoption"><span class="id" title="inductive">natoption</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Lists.html#d:132"><span class="id" title="variable">d</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#PartialMap.empty"><span class="id" title="constructor">empty</span></a>         ⇒ <a class="idref" href="Lists.html#NatList.None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Lists.html#PartialMap.record"><span class="id" title="constructor">record</span></a> <span class="id" title="var">y</span> <span class="id" title="var">v</span> <span class="id" title="var">d'</span> ⇒ <span class="id" title="keyword">if</span> <a class="idref" href="Lists.html#eqb_id"><span class="id" title="definition">eqb_id</span></a> <a class="idref" href="Lists.html#x:131"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">then</span> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">v</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="Lists.html#find:133"><span class="id" title="definition">find</span></a> <a class="idref" href="Lists.html#x:131"><span class="id" title="variable">x</span></a> <span class="id" title="var">d'</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab99"></a><h4 class="section">Exercise: 1 star, standard (update_eq)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="PartialMap.update_eq" class="idref" href="#PartialMap.update_eq"><span class="id" title="lemma">update_eq</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> (<a id="d:135" class="idref" href="#d:135"><span class="id" title="binder">d</span></a> : <a class="idref" href="Lists.html#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a>) (<a id="x:136" class="idref" href="#x:136"><span class="id" title="binder">x</span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) (<a id="v:137" class="idref" href="#v:137"><span class="id" title="binder">v</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Lists.html#PartialMap.find"><span class="id" title="definition">find</span></a> <a class="idref" href="Lists.html#x:136"><span class="id" title="variable">x</span></a> (<a class="idref" href="Lists.html#PartialMap.update"><span class="id" title="definition">update</span></a> <a class="idref" href="Lists.html#d:135"><span class="id" title="variable">d</span></a> <a class="idref" href="Lists.html#x:136"><span class="id" title="variable">x</span></a> <a class="idref" href="Lists.html#v:137"><span class="id" title="variable">v</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#NatList.Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Lists.html#v:137"><span class="id" title="variable">v</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab100"></a><h4 class="section">Exercise: 1 star, standard (update_neq)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="PartialMap.update_neq" class="idref" href="#PartialMap.update_neq"><span class="id" title="lemma">update_neq</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> (<a id="d:138" class="idref" href="#d:138"><span class="id" title="binder">d</span></a> : <a class="idref" href="Lists.html#PartialMap.partial_map"><span class="id" title="inductive">partial_map</span></a>) (<a id="x:139" class="idref" href="#x:139"><span class="id" title="binder">x</span></a> <a id="y:140" class="idref" href="#y:140"><span class="id" title="binder">y</span></a> : <a class="idref" href="Lists.html#id"><span class="id" title="inductive">id</span></a>) (<a id="o:141" class="idref" href="#o:141"><span class="id" title="binder">o</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Lists.html#eqb_id"><span class="id" title="definition">eqb_id</span></a> <a class="idref" href="Lists.html#x:139"><span class="id" title="variable">x</span></a> <a class="idref" href="Lists.html#y:140"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Lists.html#PartialMap.find"><span class="id" title="definition">find</span></a> <a class="idref" href="Lists.html#x:139"><span class="id" title="variable">x</span></a> (<a class="idref" href="Lists.html#PartialMap.update"><span class="id" title="definition">update</span></a> <a class="idref" href="Lists.html#d:138"><span class="id" title="variable">d</span></a> <a class="idref" href="Lists.html#y:140"><span class="id" title="variable">y</span></a> <a class="idref" href="Lists.html#o:141"><span class="id" title="variable">o</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Lists.html#PartialMap.find"><span class="id" title="definition">find</span></a> <a class="idref" href="Lists.html#x:139"><span class="id" title="variable">x</span></a> <a class="idref" href="Lists.html#d:138"><span class="id" title="variable">d</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">
<span class="id" title="keyword">End</span> <a class="idref" href="Lists.html#PartialMap"><span class="id" title="module">PartialMap</span></a>.<br/>
</div>

<div class="doc">
<a id="lab101"></a><h4 class="section">Exercise: 2 stars, standard, optional (baz_num_elts)</h4>
 Consider the following inductive definition: 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="baz" class="idref" href="#baz"><span class="id" title="inductive">baz</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="Baz1" class="idref" href="#Baz1"><span class="id" title="constructor">Baz1</span></a> (<a id="x:144" class="idref" href="#x:144"><span class="id" title="binder">x</span></a> : <a class="idref" href="Lists.html#baz:142"><span class="id" title="inductive">baz</span></a>)<br/>
&nbsp;&nbsp;| <a id="Baz2" class="idref" href="#Baz2"><span class="id" title="constructor">Baz2</span></a> (<a id="y:145" class="idref" href="#y:145"><span class="id" title="binder">y</span></a> : <a class="idref" href="Lists.html#baz:142"><span class="id" title="inductive">baz</span></a>) (<a id="b:146" class="idref" href="#b:146"><span class="id" title="binder">b</span></a> : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>).<br/>
</div>

<div class="doc">
How <i>many</i> elements does the type <span class="inlinecode"><span class="id" title="var">baz</span></span> have? (Explain in words,
    in a comment.) 
</div>
<div class="code">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_baz_num_elts" class="idref" href="#manual_grade_for_baz_num_elts"><span class="id" title="definition">manual_grade_for_baz_num_elts</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<span class="comment">(*&nbsp;2021-08-11&nbsp;15:08&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>